4.5 Timed Zenoness Checking

4.5 Timed Zenoness Checking

Because RTS module supports process constructs like deadline, it suffers from zeno executions, i.e., infinitely many steps taking within finite time. Zeno executions are unrealistic and therefore must be ruled out in model checking. It is known that zone graphs are not fine enough to distinguish zeno executions. We show that the zone graph produced by dynamic zone abstraction can be modified so that the properties are verified with the assumption of non-Zenoness.

To remove zeno executions, PAT implements zeno checking for LTL and deadlock assertions. Users only need to tick the "Apply Zeno Check" in the model checking form.